(declare-fun userAgent () String)
(declare-fun |0 Fill 0| () String)
(declare-fun |0 Fill 1| () String)
(declare-fun |0 Fill 2| () String)
(declare-fun |0 Fill 3| () String)
(declare-fun |0 Fill 4| () String)
(declare-fun |0 Fill 6| () String)
(declare-fun |0 Fill 5| () String)
(declare-fun / (S+) s+Safari/_0)
(check-sat)
